a(a(append, nil), ys) → ys
a(a(append, a(a(cons, x), xs)), ys) → a(a(cons, x), a(a(append, xs), ys))
a(a(filter, f), nil) → nil
a(a(filter, f), a(a(cons, x), xs)) → a(a(a(if, a(f, x)), x), a(a(filter, f), xs))
a(a(le, 0), y) → true
a(a(le, a(s, x)), 0) → false
a(a(le, a(s, x)), a(s, y)) → a(a(le, x), y)
a(a(a(if, true), x), xs) → a(a(cons, x), xs)
a(a(a(if, false), x), xs) → xs
a(a(not, f), b) → a(not2, a(f, b))
a(not2, true) → false
a(not2, false) → true
a(qs, nil) → nil
a(qs, a(a(cons, x), xs)) → a(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs))))
↳ QTRS
↳ DependencyPairsProof
a(a(append, nil), ys) → ys
a(a(append, a(a(cons, x), xs)), ys) → a(a(cons, x), a(a(append, xs), ys))
a(a(filter, f), nil) → nil
a(a(filter, f), a(a(cons, x), xs)) → a(a(a(if, a(f, x)), x), a(a(filter, f), xs))
a(a(le, 0), y) → true
a(a(le, a(s, x)), 0) → false
a(a(le, a(s, x)), a(s, y)) → a(a(le, x), y)
a(a(a(if, true), x), xs) → a(a(cons, x), xs)
a(a(a(if, false), x), xs) → xs
a(a(not, f), b) → a(not2, a(f, b))
a(not2, true) → false
a(not2, false) → true
a(qs, nil) → nil
a(qs, a(a(cons, x), xs)) → a(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs))))
A(qs, a(a(cons, x), xs)) → A(not, a(le, x))
A(a(append, a(a(cons, x), xs)), ys) → A(a(cons, x), a(a(append, xs), ys))
A(qs, a(a(cons, x), xs)) → A(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs))))
A(qs, a(a(cons, x), xs)) → A(le, x)
A(qs, a(a(cons, x), xs)) → A(append, a(qs, a(a(filter, a(le, x)), xs)))
A(a(a(if, true), x), xs) → A(cons, x)
A(a(a(if, true), x), xs) → A(a(cons, x), xs)
A(a(filter, f), a(a(cons, x), xs)) → A(a(a(if, a(f, x)), x), a(a(filter, f), xs))
A(qs, a(a(cons, x), xs)) → A(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs)))
A(a(le, a(s, x)), a(s, y)) → A(a(le, x), y)
A(a(append, a(a(cons, x), xs)), ys) → A(a(append, xs), ys)
A(qs, a(a(cons, x), xs)) → A(filter, a(le, x))
A(a(le, a(s, x)), a(s, y)) → A(le, x)
A(a(filter, f), a(a(cons, x), xs)) → A(a(filter, f), xs)
A(a(append, a(a(cons, x), xs)), ys) → A(append, xs)
A(qs, a(a(cons, x), xs)) → A(qs, a(a(filter, a(le, x)), xs))
A(qs, a(a(cons, x), xs)) → A(a(filter, a(le, x)), xs)
A(qs, a(a(cons, x), xs)) → A(qs, a(a(filter, a(not, a(le, x))), xs))
A(a(not, f), b) → A(not2, a(f, b))
A(a(filter, f), a(a(cons, x), xs)) → A(f, x)
A(qs, a(a(cons, x), xs)) → A(filter, a(not, a(le, x)))
A(qs, a(a(cons, x), xs)) → A(a(filter, a(not, a(le, x))), xs)
A(a(filter, f), a(a(cons, x), xs)) → A(a(if, a(f, x)), x)
A(a(not, f), b) → A(f, b)
A(a(filter, f), a(a(cons, x), xs)) → A(if, a(f, x))
a(a(append, nil), ys) → ys
a(a(append, a(a(cons, x), xs)), ys) → a(a(cons, x), a(a(append, xs), ys))
a(a(filter, f), nil) → nil
a(a(filter, f), a(a(cons, x), xs)) → a(a(a(if, a(f, x)), x), a(a(filter, f), xs))
a(a(le, 0), y) → true
a(a(le, a(s, x)), 0) → false
a(a(le, a(s, x)), a(s, y)) → a(a(le, x), y)
a(a(a(if, true), x), xs) → a(a(cons, x), xs)
a(a(a(if, false), x), xs) → xs
a(a(not, f), b) → a(not2, a(f, b))
a(not2, true) → false
a(not2, false) → true
a(qs, nil) → nil
a(qs, a(a(cons, x), xs)) → a(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
A(qs, a(a(cons, x), xs)) → A(not, a(le, x))
A(a(append, a(a(cons, x), xs)), ys) → A(a(cons, x), a(a(append, xs), ys))
A(qs, a(a(cons, x), xs)) → A(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs))))
A(qs, a(a(cons, x), xs)) → A(le, x)
A(qs, a(a(cons, x), xs)) → A(append, a(qs, a(a(filter, a(le, x)), xs)))
A(a(a(if, true), x), xs) → A(cons, x)
A(a(a(if, true), x), xs) → A(a(cons, x), xs)
A(a(filter, f), a(a(cons, x), xs)) → A(a(a(if, a(f, x)), x), a(a(filter, f), xs))
A(qs, a(a(cons, x), xs)) → A(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs)))
A(a(le, a(s, x)), a(s, y)) → A(a(le, x), y)
A(a(append, a(a(cons, x), xs)), ys) → A(a(append, xs), ys)
A(qs, a(a(cons, x), xs)) → A(filter, a(le, x))
A(a(le, a(s, x)), a(s, y)) → A(le, x)
A(a(filter, f), a(a(cons, x), xs)) → A(a(filter, f), xs)
A(a(append, a(a(cons, x), xs)), ys) → A(append, xs)
A(qs, a(a(cons, x), xs)) → A(qs, a(a(filter, a(le, x)), xs))
A(qs, a(a(cons, x), xs)) → A(a(filter, a(le, x)), xs)
A(qs, a(a(cons, x), xs)) → A(qs, a(a(filter, a(not, a(le, x))), xs))
A(a(not, f), b) → A(not2, a(f, b))
A(a(filter, f), a(a(cons, x), xs)) → A(f, x)
A(qs, a(a(cons, x), xs)) → A(filter, a(not, a(le, x)))
A(qs, a(a(cons, x), xs)) → A(a(filter, a(not, a(le, x))), xs)
A(a(filter, f), a(a(cons, x), xs)) → A(a(if, a(f, x)), x)
A(a(not, f), b) → A(f, b)
A(a(filter, f), a(a(cons, x), xs)) → A(if, a(f, x))
a(a(append, nil), ys) → ys
a(a(append, a(a(cons, x), xs)), ys) → a(a(cons, x), a(a(append, xs), ys))
a(a(filter, f), nil) → nil
a(a(filter, f), a(a(cons, x), xs)) → a(a(a(if, a(f, x)), x), a(a(filter, f), xs))
a(a(le, 0), y) → true
a(a(le, a(s, x)), 0) → false
a(a(le, a(s, x)), a(s, y)) → a(a(le, x), y)
a(a(a(if, true), x), xs) → a(a(cons, x), xs)
a(a(a(if, false), x), xs) → xs
a(a(not, f), b) → a(not2, a(f, b))
a(not2, true) → false
a(not2, false) → true
a(qs, nil) → nil
a(qs, a(a(cons, x), xs)) → a(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
A(a(le, a(s, x)), a(s, y)) → A(a(le, x), y)
a(a(append, nil), ys) → ys
a(a(append, a(a(cons, x), xs)), ys) → a(a(cons, x), a(a(append, xs), ys))
a(a(filter, f), nil) → nil
a(a(filter, f), a(a(cons, x), xs)) → a(a(a(if, a(f, x)), x), a(a(filter, f), xs))
a(a(le, 0), y) → true
a(a(le, a(s, x)), 0) → false
a(a(le, a(s, x)), a(s, y)) → a(a(le, x), y)
a(a(a(if, true), x), xs) → a(a(cons, x), xs)
a(a(a(if, false), x), xs) → xs
a(a(not, f), b) → a(not2, a(f, b))
a(not2, true) → false
a(not2, false) → true
a(qs, nil) → nil
a(qs, a(a(cons, x), xs)) → a(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
A(a(le, a(s, x)), a(s, y)) → A(a(le, x), y)
The value of delta used in the strict ordering is 6.
POL(a(x1, x2)) = 2 + (2)x_2
POL(A(x1, x2)) = (3)x_2
POL(s) = 0
POL(le) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
a(a(append, nil), ys) → ys
a(a(append, a(a(cons, x), xs)), ys) → a(a(cons, x), a(a(append, xs), ys))
a(a(filter, f), nil) → nil
a(a(filter, f), a(a(cons, x), xs)) → a(a(a(if, a(f, x)), x), a(a(filter, f), xs))
a(a(le, 0), y) → true
a(a(le, a(s, x)), 0) → false
a(a(le, a(s, x)), a(s, y)) → a(a(le, x), y)
a(a(a(if, true), x), xs) → a(a(cons, x), xs)
a(a(a(if, false), x), xs) → xs
a(a(not, f), b) → a(not2, a(f, b))
a(not2, true) → false
a(not2, false) → true
a(qs, nil) → nil
a(qs, a(a(cons, x), xs)) → a(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
A(a(append, a(a(cons, x), xs)), ys) → A(a(append, xs), ys)
a(a(append, nil), ys) → ys
a(a(append, a(a(cons, x), xs)), ys) → a(a(cons, x), a(a(append, xs), ys))
a(a(filter, f), nil) → nil
a(a(filter, f), a(a(cons, x), xs)) → a(a(a(if, a(f, x)), x), a(a(filter, f), xs))
a(a(le, 0), y) → true
a(a(le, a(s, x)), 0) → false
a(a(le, a(s, x)), a(s, y)) → a(a(le, x), y)
a(a(a(if, true), x), xs) → a(a(cons, x), xs)
a(a(a(if, false), x), xs) → xs
a(a(not, f), b) → a(not2, a(f, b))
a(not2, true) → false
a(not2, false) → true
a(qs, nil) → nil
a(qs, a(a(cons, x), xs)) → a(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
A(a(append, a(a(cons, x), xs)), ys) → A(a(append, xs), ys)
The value of delta used in the strict ordering is 12.
POL(append) = 0
POL(cons) = 2
POL(a(x1, x2)) = 1 + (3)x_2
POL(A(x1, x2)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
a(a(append, nil), ys) → ys
a(a(append, a(a(cons, x), xs)), ys) → a(a(cons, x), a(a(append, xs), ys))
a(a(filter, f), nil) → nil
a(a(filter, f), a(a(cons, x), xs)) → a(a(a(if, a(f, x)), x), a(a(filter, f), xs))
a(a(le, 0), y) → true
a(a(le, a(s, x)), 0) → false
a(a(le, a(s, x)), a(s, y)) → a(a(le, x), y)
a(a(a(if, true), x), xs) → a(a(cons, x), xs)
a(a(a(if, false), x), xs) → xs
a(a(not, f), b) → a(not2, a(f, b))
a(not2, true) → false
a(not2, false) → true
a(qs, nil) → nil
a(qs, a(a(cons, x), xs)) → a(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
A(qs, a(a(cons, x), xs)) → A(a(filter, a(not, a(le, x))), xs)
A(a(filter, f), a(a(cons, x), xs)) → A(a(filter, f), xs)
A(qs, a(a(cons, x), xs)) → A(a(filter, a(le, x)), xs)
A(qs, a(a(cons, x), xs)) → A(qs, a(a(filter, a(le, x)), xs))
A(qs, a(a(cons, x), xs)) → A(qs, a(a(filter, a(not, a(le, x))), xs))
A(a(not, f), b) → A(f, b)
A(a(filter, f), a(a(cons, x), xs)) → A(f, x)
a(a(append, nil), ys) → ys
a(a(append, a(a(cons, x), xs)), ys) → a(a(cons, x), a(a(append, xs), ys))
a(a(filter, f), nil) → nil
a(a(filter, f), a(a(cons, x), xs)) → a(a(a(if, a(f, x)), x), a(a(filter, f), xs))
a(a(le, 0), y) → true
a(a(le, a(s, x)), 0) → false
a(a(le, a(s, x)), a(s, y)) → a(a(le, x), y)
a(a(a(if, true), x), xs) → a(a(cons, x), xs)
a(a(a(if, false), x), xs) → xs
a(a(not, f), b) → a(not2, a(f, b))
a(not2, true) → false
a(not2, false) → true
a(qs, nil) → nil
a(qs, a(a(cons, x), xs)) → a(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs))))